Nuprl Definition : es-pred! 11,40

es-pred!(esee') == pred!(e;e'
latex



clarification:

es-pred!(esee') == pred!(es-E(es);es-pred?(es);es_info(es);e;e'
latex


Definitionspred!(e;e'), es-E(es), es-pred?(es), es_info(es)
FDL editor aliaseses-pred!

origin